Inference at * 1 
Iof proof for Lemma nth tl is fseg:



1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. L2 = (L @ L1)
  n:{0..(||L2||+1)}. (L1 = nth_tl(n;L2)) 

latex

 by InteriorProof ((((((((HypSubst (-1) 0) 
CollapseTHENM (RWO "length_append" 0))) 

CollapseTHENM (RWO CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
CollapseTHENM (RWO)) (first_tok SupInf:t) inil_term)))) 
CollapseTHEN (InstConcl [||L||]))) 

CollapseTHEN (InstCCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
CollapseTHEN (Inst)) (first_tok SupInf:t) inil_term))) 

latex

C1: 

C1:   L1 = nth_tl(||L||;L @ L1)
C.

Definitions	||as||, P  Q, P  Q, x:A. B(x), #$n, S  T, |g|, i  j < k, P & Q, x:A  B(x), , T, True, A, False, P  Q, a < b, n+m, i  j , A  B, , nth_tl(n;as), x:A. B(x), x:AB(x), , {x:A| B(x)} , t  T, as @ bs, {i..j}, s = t, Type, type List
Lemmas	iff wf, rev implies wf, squash wf, true wf, add functionality wrt eq, length append, append wf, int seg wf, length wf nat, nat wf, le wf, non neg length, length wf1, nth tl wf